es:ES, l:IdLnk, tg:Id, T:Type.
({m:Msg| source(mlnk(m)) = source(l)  Id} 
({mr Msg(l',tg'. if l' = l  tg' = tg then T else Top fi ))
 (e:E. (isrcv(e))  (lnk(e) = l)  (tag(e) = tg)  (valtype(e) r T)) 

latex

Definitions	x:A. B(x), P  Q, if b then t else f fi , valtype(e), t  T, tt, ff, , , Unit, P  Q, P & Q, A, False,
Lemmas	bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Id wf, es-tag wf, IdLnk wf, es-lnk wf, es-isrcv wf, es-E wf, es-Msg wf, lsrc wf, mlnk wf2, Msg wf, ifthenelse wf, band wf, eq lnk wf, eq id wf, top wf, event system wf